da:k:Knd fp Type, k:Knd. Normal(da)  k  dom(da)  Normal(da(k)?Void) 

latex

Definitions	False, P  Q, A, t  T, x:A. B(x), b, b, , s = t, Prop, Knd, Type, x.A(x), x. t(x), Top, a:A fp B(a), x:AB(x), KindDeq, x  dom(f), x:AB(x), P & Q, P  Q, Unit, left+right, f(x), Normal(T), Void, if b t else f fi, xdom(f). v=f(x)   P(x;v), f(x)?z, Normal(da)
Lemmas	normal-type wf, fpf-ap wf, fpf wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, Knd wf, bool wf, bnot wf, not wf, assert wf